#include "model.hpp"
#include <iostream>

Changes::Changes() : deviceOldNewPort(Device::cnt) { }

void Changes::insert(BDD &delta, Port * const oldPort, Port * const newPort) {
    LACE_ME;

    unordered_map<Port*, unordered_map<Port*, BDD> > &oldPortTo = deviceOldNewPort[oldPort->device->uid];
    unordered_map<Port*, BDD> &newPortToBdd = oldPortTo[oldPort];
    if (newPortToBdd.find(newPort) == newPortToBdd.end()) {
        newPortToBdd[newPort] = delta;
        mtbdd_protect(&newPortToBdd[newPort]);
    } else {
        newPortToBdd[newPort] = sylvan_or(newPortToBdd[newPort], delta);
    }
}

void Changes::clean() {
    deviceOldNewPort.clear();
    deviceOldNewPort.resize(Device::cnt);
}

Model::Model(const Network &network) {
    LACE_ME;
    for (int i = 0; i < 32; i ++) {
        bit[i] = sylvan_ithvar(i);
        mtbdd_protect(bit + i);
    }

    vector<Port*> ports(Device::cnt);
    // Initialize each device with default rule sending packets to default device (i.e., black-hole)
    for (auto entry : network.nameToDevice) {
        if (entry.first == "default") continue;
        Device * const device = entry.second;
        Port *defaultPort = device->addPortByName( device->name + "-default");
        Rule *rule = new Rule {.device = device, .dstIp = 0, .priority = 0, .port = defaultPort};
        identifyChangesInsert(rule);
        // initializing default rules w/o generating changes
        ports[device->uid] = defaultPort;
    }
    PEC *predicate = new PEC(ports);
    predicates[*predicate] = sylvan_true;
    mtbdd_protect(&predicates[*predicate] );
    for (Port* port : ports) {
        portToPECs[port].insert(*predicate);
    }
    changes.clean();
}

void Model::insertMiniBatch(vector<Rule*> rules) {
    sort(rules.begin(), rules.end(),
         [](const Rule * a, const Rule * b) -> bool {
        return a->priority > b->priority; });
    for (Rule *rule : rules) {
        identifyChangesInsert(rule);
    }
}

void Model::identifyChangesInsert(Rule *rule) {
    LACE_ME;

    rule->hit = sylvan_true;
    mtbdd_protect(&rule->hit);
    for (int i = 0; i < rule->priority; i++) {
        if ((rule->dstIp >> (31 - i)) & 1L) {
            rule->hit = sylvan_and(rule->hit, bit[i]);
        } else {
            rule->hit = sylvan_diff(rule->hit, bit[i]);
        }
    }
    rule->nMatch = sylvan_not(rule->hit);
    mtbdd_protect(&rule->nMatch);

    for (Rule *r : rule->device->addAndGetAllRulesUntil(rule)) {
        if (r->priority > rule->priority) rule->hit = sylvan_diff(rule->hit, r->hit);

        if (rule->hit == sylvan_false) return;

        if (r->priority < rule->priority) {
            BDD intersection = sylvan_and(r->hit, rule->hit);
            mtbdd_protect(&intersection);

            if (r->port != rule->port) changes.insert(intersection, r->port, rule->port);

            r->hit = sylvan_diff(r->hit, intersection);
            mtbdd_unprotect(&intersection);
        }
    }
}

int Model::changeSize() {
    int ret = 0;
    for (auto entryI: changes.deviceOldNewPort) {
        for (auto entryJ : entryI) ret += entryJ.second.size();
    }
    return ret;
}

int Model::predicateSize() {
    return predicates.size();
}

void Model::consumeChanges() {
    LACE_ME;

    for (auto &entryI : changes.deviceOldNewPort) { // for each device
        unordered_map<PEC, BDD, PECHasher> delta;
        for (auto &entryJ : entryI) {
            // cout << "start action " << entryJ.first->name << " for device " << entryJ.first->device->name << endl;
            // cout << entryJ.second.size() << endl;
            Port * const &oldPort = entryJ.first;
            for (auto &entryK : entryJ.second) {
                Port * const &newPort = entryK.first;
                BDD const &p = entryK.second;
                for (const PEC &from : portToPECs[oldPort]) {
                    BDD intersection = sylvan_and(predicates[from], p);
                    if (intersection == sylvan_false) continue;

                    mtbdd_protect(&intersection);

                    if (delta.find(from) == delta.end()) {
                        delta[from] = intersection;
                        mtbdd_protect(&delta[from]);
                    } else {
                        delta[from] = sylvan_or(delta[from], intersection);
                    }

                    PEC to(from.ports);
                    to.ports[newPort->device->uid] = newPort;
                    auto it = predicates.find(to);
                    if (it == predicates.end()) {
                        predicates[to] = intersection;
                        sylvan_protect(&predicates[to]);
                        for (Port * &pt : to.ports) portToPECs[pt].insert(to);
                    } else {
                        if (delta.find(to) == delta.end()) {
                            delta[to] = intersection;
                            mtbdd_protect(&delta[to]);
                        } else {
                            delta[to] = sylvan_or(delta[to], intersection);
                        }
                    }

                    mtbdd_unprotect(&intersection);
                }
            }
        }

        for (auto &entry : delta) {
            predicates[entry.first] = sylvan_xor(predicates[entry.first], entry.second);
            if (predicates[entry.first] == sylvan_false) {
                mtbdd_unprotect(&predicates[entry.first]);
                for (Port * const &pt : entry.first.ports) portToPECs[pt].erase(entry.first);
                predicates.erase(entry.first);
            }
            mtbdd_unprotect(&entry.second);
        }
        delta.clear();
        // cout << predicates.size() << endl;
    }
    changes.clean();
}